Two worries with this approach:

• Can you define a RawFoldable for Vec?
• Can you show that FoldMap is monoid homomorphism for commutative monoids from Lists up to permutations?

@Taneb thanks for the rapid feedback!

Two worries with this approach:

It's definitely DRAFT, but I appreciate the nudge to think about extensibility of the design.

* Can you define a `RawFoldable` for `Vec`?

In the first instance (sic), surely only a non-dependent one (see latest commits). In general, I might expect the design to evolve to embrace:

• Effect.Indexed.Foldable , based on the introduction of
• Algebra.Graded.*, so that I can introduce graded monoids, and then generalise foldMap to take such a thing, and then use that Vec; []; _++_ is graded over ℕ; 0; _+_...?
• UPDATED: or else to consider indexed monoids (cf. vectors of composable maps)?

* Can you show that FoldMap is monoid homomorphism for _commutative_ monoids from Lists up to permutations?

For sure, I've given much less thought to the Setoid structure on the (Raw)Monoid argument being passed in, nor to the way properties of a RawFoldable* might cash out as an IsFoldable 'structure'. But I felt I had some liberty here, given that we (still!) haven't stabilised on how to go beyond RawFunctor to Functor with laws...

Thinking about graded monoids feels like a long path that ends up with this PR never quite getting merged... and I don't want that. (e.g. for some types, the right kind of "monoid" might be a category). Actually, for List⁺, you'd want to use Semigroup, and for Maybe you'd want to use Pointed...

The reason I asked about commutative structures is that the original reason I wanted foldMap was because it felt like the right way to say that sum respects permutation - I've defined something similar in #1969 for product here

I'm also going to point out the connection to #1962: foldMap for List is part of the proof that List is (a representation of) the free monoid for some set.

@Taneb thanks for the feedback.

I think I'm not clear whether what you are asking for (and proposing in #1281) was the haskell-style foldMap/fold API of Foldable (which is tied to Monoid instances), or to generalise it so that foldMap is always the canonical extension map associated with a Free construction.

If the latter, that's a different kettle of fish (and yes, #1962 is one prototype attempt at it, that will probably need more rounds of design discussion; the/an alternative via Church encodings does, I think need to be investigated, not least because the library currently has no purely functional equivalent to build for List... #2304 ), and not what I had been proposing here.

If the former (which this PR is concerned with), then you may not immediately see a payoff for CommutativeMonoid and List-modulo-permutation from this PR. But see also recent work from Vikraman Chowdhury and Marcelo Fiore, as well as from the Strathclyde MSPs, for further discussion of that. My own view is that we have broken Permutation from the start via a bad inductive presentation (which certainly hindered Vikraman, IIUC), but that's a topic for a separate (hobby-horse) issue... ;-)

In either case, the development for indexed containers such as Vec will require separate consideration, in any case... I am grateful for your prompt to think about it, and think it does lead naturally to graded monoids, but welcome further discussion/input on such topics. I agree I don't want to hold things up for the sake of not achieving such a target, hence my commit of the non-indexed foldMap for Vec following Foldable based solely on Monoid.

Reply about the comment on product on the PR #1969 itself... UPDATED now see also #2333 , specifically the redefinition there (not the last word, for sure, but baby steps...)

Two further comments on this evolving PR:

• I think it does serve a different/distinct purpose to that argued for by @Taneb in Add foldMap and fold #1281
• I think it is of independent interest/utility (even if following the haskell model a bit too closely), but conceivably all the functionality (for List ;-)) can be realised by suitable combinations of the monadic/applicative machinery in Data.List.Effectful precisely because Lists are one version of the underlying carrier of the free Monoid... in which case it would make sense to abandon this PR in favour of enhancing the content there.

Regarding different potential equalities on List, however, at the moment, because the only structure considered is Raw (ie no non-trivial equations on either source or target of the foldMap function, in particular what it might be taken to be a homomorphism between), I don't rule out that we couldn't also tackle @Taneb 's desire to handle (Idempotent)CommutativeMonoids as well. But I'm (still) inclined to think that that might better be handled by a systematic treatment of Free constructions cf. #1962 / #1954 and the associated discussions there.

As to the "fork in the road", I hadn't intended to force such an issue (not sure I'd realised it might even be such).

Given that progress on Algebra.Free had stalled, which I had originally thought would be the solution to the original issue, I had thought that this was/might be a comparatively much lower-hanging proposal... if not an ideal one.

DRAFT status means we can/should have the discussion before proceeding... interested in seeing more!

What am I missing? I'm seeing the word 'instance' all over the comments (and in the review) but none in the code?

What am I missing? I'm seeing the word 'instance' all over the comments (and in the review) but none in the code?

My bad, or at least, my possible misuse of the term-of-art when I should say something else, like 'dictionary'. In my mind, but not, I think (!?), unique to me, values of record type corresponding to (structures corresponding to) haskell type-classes, with such values corresponding to (dictionaries associated to) haskell instances of such classes, get called 'instance's informally...

... That said, it seems as though we have turned away from using actual {{...}} instance-based dictionary resolution for instantiating (sic) 'type-classes' in this style (there's a comment from @jespercockx somewhere on the main issue tracker to that effect) so perhaps this usage should be deprecated/avoided?

... That said, it seems as though we have turned away from using actual {{...}} instance-based dictionary resolution for instantiating (sic) 'type-classes' in this style (there's a comment from @jespercockx somewhere on the main issue tracker to that effect) so perhaps this usage should be deprecated/avoided?

AFAIK the policy is to define record values that can be used as instances but do not actually mark them with the instance keyword in the main modules. Where it is useful, there can then also be a separate .Instances module that re-exports the relevant record values as proper instances.

Thanks @jespercockx !

My bad, or at least, my possible misuse of the term-of-art when I should say something else, like 'dictionary'. In my mind, but not, I think (!?), unique to me, values of record type corresponding to (structures corresponding to) haskell type-classes, with such values corresponding to (dictionaries associated to) Haskell instances of such classes, get called 'instance's informally...

My take on this (with credit to Conor for making some of this clear): Haskell confuses two things, the idea of an interface, and the algorithm for giving implementations of that interface by search. So Haskell's typeclasses are the only mechanism for creating interfaces, which then push you into implicit resolution for implementations. That begets orphans, useless newtype, etc. The apparent convenience eventually engenders more pain once you reach a large enough scale.

In Agda, record types are rich enough to act as interfaces. So while it is indeed tempting to call an actual record an 'instance', as Agda also has Haskell-style typeclasses, that just leads to confusion. So I think Agda-speak has evolved to only call 'instance' those things that use instance explicitly.